D:Dsys, i:Id, s:M(i).state, k:Knd, v:d-decl(D;i)(k).
Feasible(D)  next-world-state(D;i;s;k;v)  d-world-state(D;i) 

latex

Definitions	x:A. B(x), P  Q, t  T, d-world-state(D;i), next-world-state(D;i;s;k;v), M.state, State(ds), Feasible(D), P & Q, Prop, P  Q, M.ds(x)
Lemmas	d-decl-subtype, IdLnk wf, filter type, ma-msg wf, eq id wf, lsrc wf, mlnk wf d, ma-send-val wf, d-feasible wf, d-decl wf, Knd wf, ma-st wf, d-m wf, Id wf, dsys wf, ma-ef-val wf, doact wf, subtype rel list, assert wf, assert-eq-id